| Definitions | Top, t  T, type List,  x:A. B(x), a:A fp B(a), x:A B(x), IdLnk, Void,  x.A(x), 2of(t), rcv(l,tg), f(x)?z, 1of(t), Valtype(da;k), x:A B(x), , f  g, State(ds), Prop, locl(a), <a,b>, mk-ma, , MsgA, M1 M2, s = t, KindDeq, Type,  x. t(x), Knd, lexpr{i}, IdDeq, Id, P   Q, P  Q, P & Q, P Q, IdLnkDeq, product-deq(A;B;a;b), True,  T, f(a), x(s), EqDecider(T),  x:A. B(x), Atom$n, left+right, strong-subtype(A;B), S  T, S  T |